(set-option :trace true) 
(set-option :smt.random_seed 1)  
(declare-fun a () Int) 
(declare-fun b () Int) 
(declare-fun c () Int) 
(declare-fun d () Int) 
(declare-fun h () Int) 
(declare-fun e () Int) 
(declare-fun f () Int)  
(declare-fun g () Int) 
(declare-fun i () Int) 
(assert (and (or (not (<= 6 e)) (= e (+ (* (/ d i)) 2) 0)) 
(= (not (<= (+ (+ (/ a (/ b h)))) 6)) (= (+ (+ f (/ d i))) 0)) 
(= (+ (* (/ c g))) 1)))
(check-sat)   